% !Mode:: "TeX:UTF-8"
% !TeX root = ../rslbook.tex

\head{Описание сигнатуры функции на RSL}

\begin{lstlisting}
value add: Int >< Int -~-> Int
\end{lstlisting}
Имеется одна функция add с двумя аргументами типа $\Int$ (аргументы разделяются символом $\NonDetermFn$). Функция вычисляет одно значение и это значение типа $\Int$ (несколько значений так же разделяются символом $\times$). Функция не имеет побочного эффекта.

\head{Описание алгоритма целиком}
\begin{lstlisting}
value add: Int >< Int -~-> Int
add(x,y) is x+y
\end{lstlisting}
После сигнатуры идет тело функции. Вначале идет имя функции с формальными параметрами, затем символ $\Is$ и затем выражение. Вычислением функции является вычисление этого выражения (в данном случае, сложение двух чисел-аргументов).

\head{Встроенные типы}
\textbf{Int}, \textbf{Nat}, \textbf{Real}, \textbf{Bool}, \textbf{Char}, \textbf{Text}, \textbf{Unit}.

Тип \textbf{Int} содержит в себе все возможные целые числа. Ограничений на их значения (типа MAXINT) нет.

Тип \textbf{Nat} содержит число 0 и все возможные положительные целые числа. Ограничений сверху на их значения нет. Тип поддерживает все операции, определенные для типа \textbf{Int}.

Тип \textbf{Real} содержит в себе все возможные вещественные числа. Важно понимать, что эти числа являются математической абстракцией тех вещественных чисел, которые представимы в архитектуре компьютера. Тип \textbf{Real} --- это те числа, с которыми работают математики. Следовательно, они включают и все вещественные числа, представимые в какой-угодно архитектуре компьютера. Например, в этом типе есть число <<квадратный корень из двух>>.

Тип \textbf{Bool} содержит булевские значения \textbf{true} и \textbf{false}.

Тип \textbf{Char} содержит все возможные отдельные символы. Этот тип не привязан ни к одной из кодировок (поскольку этот тип --- лишь математическая абстракция). Этот тип содержит все мыслимые символы. Поэтому не определена операция получения <<кода символа>>, привычная для многих языков программирования.

Тип \textbf{Text} является массивом символов (о массивах см.ниже).

Тип \textbf{Unit} является специальным и используется для ограниченного количества случаев (см.ниже). Основное применение --- то же, какое имеет ключевое слово \texttt{void} в сигнатурах функций языка Си.

\head{Операции над встроенными типами}
Арифметические:
\begin{lstlisting}
value
  +: Int >< Int -> Int,
  -: Int >< Int -> Int,
  *: Int >< Int -> Int,
  /: Int >< Int -~-> Int,
  \: Int >< Int -~-> Int,
  **: Int >< Int -~-> Int,
  abs: Int -> Nat,
  real: Int -> Real,

  +: Real >< Real -> Real,
  -: Real >< Real -> Real,
  *: Real >< Real -> Real,
  /: Real >< Real -~-> Real,
  **: Real >< Real -~-> Real,
  abs: Real -> Real,
  int: Real -> Int,

  <: Int >< Int -> Bool,
  <=: Int >< Int -> Bool,
  >: Int >< Int -> Bool,
  >=: Int >< Int -> Bool,

  <: Real >< Real -> Bool,
  <=: Real >< Real -> Bool,
  >: Real >< Real -> Bool,
  >=: Real >< Real -> Bool,

  ~: Bool       -> Bool,
  /\: Bool >< Bool -> Bool,
  \/: Bool >< Bool -> Bool,
  =>: Bool >< Bool -> Bool,
\end{lstlisting}

Для любого типа определены операции сравнения на равенство:
\begin{lstlisting}
type T
value
  = : T >< T -> Bool,
  ~= : T >< T -> Bool
\end{lstlisting}

Порядок вычисления операций строго определен: сначала первый аргумент, затем, если необходимо, второй и т.д.

Логика короткая. Это означает, например, что если первый аргумент конъюнкции равен \textbf{false}, то второй аргумент не вычисляется и вся конъюнкция принимает значение \textbf{false}.

\head{Глобальные переменные}
Кроме своих аргументов функция может оперировать глобальными переменными. Каждая глобальная переменная должна быть определена в разделе \textbf{variable}, а в сигнатуре функции должен быть указан режим работы функции с переменной: по чтению или по записи-чтению. Функции разрешено оперировать лишь с теми глобальными переменными, которые указаны в сигнатуре. Например,
\begin{lstlisting}
variable status : Text
value
  init : Unit -~-> write status Unit
  init() is (status := "initialized")	
\end{lstlisting}

Функция \texttt{init} не имеет аргументов --- для указания этого факта перед стрелкой в сигнатуре функции указан тип \textbf{Unit}. Также у функции нет и возвращаемого значения --- она лишь изменяет значение глобальной переменной \texttt{status}. Этот факт также указан типом \textbf{Unit} в качестве типа возвращаемого значения.

Еще пример:
\begin{lstlisting}[escapechar={|}]
variable status : Text
value
  |is\_initialized| : Unit -~-> read status Bool
  |is\_initialized|() is
	(status = "initialized")	
\end{lstlisting}

Здесь глобальная переменная лишь читается в функции, поэтому в сигнатуре переменная \texttt{status} указана с модификатором \textbf{read}.

Можно указать в сигнатуре, что функция может читать или изменять любую глобальную переменную. В этом случае вместо имени переменной в сигнатуре функции надо написать ключевое слово \textbf{any}.

\head{Выражения}
Тело функции является выражением того типа, какой должна возвращать функция. Например, функция
\begin{lstlisting}
value f: Int -~-> Int
      f(x) is
	       x+1
\end{lstlisting}
возвращает значение типа \textbf{Int}. Ее тело состоит из суммы целых чисел, а сумма возвращает значение типа Int. Этой \textbf{математической} функции соответствует, например, следующая функция на языке Си:
\begin{lstlisting}
int f( int x )
{
    return x+1;
}
\end{lstlisting}

Однако стоит понимать следующее различие: в языке Си значения практически всех типов ограничены, а в языке RSL неограничены. Поэтому вычисление выражения x+1 в программе на Си может привести к переполнению и, поэтому, неверному с точки зрения математического определения операции <<+1>> результату.

Кроме возврата значения такого простого выражения язык RSL допускает более сложные управляющие структуры. Они составляются из более простых выражений. К таким простым выражениям относятся:
\begin{itemize}
\item встроенные операции:
\begin{lstlisting}
value f: Int -~-> Int
      f(x) is x+1
\end{lstlisting}

\item вызов другой функции (со статической проверкой типов аргументов):
\begin{lstlisting}
value g: Int -~-> Int
      g(x) is 2 * f(x-1)
\end{lstlisting}

\item условный оператор: \textbf{if} логическое выражение \textbf{then} выражение1 \textbf{else} выражение2 \textbf{end} --- типы выражений <<выражение1>> и <<выражение2>> должны совпадать --- условный оператор возвращает значение этого же типа (значение одного из выражений, в зависимости от значения логического выражения):
\begin{lstlisting}
value
   Abs: Int -~-> Nat
   Abs(x) is if x > 0 then x else -x end
\end{lstlisting}

Условный оператор без \textbf{else} --- он допустим только в случае, если <<выражение1>> имеет тип \textbf{Unit}:
\begin{lstlisting}
variable status: Text
value
   init: Bool -~-> write status Unit
   init(needed) is
     if needed then status := "initialized" end
\end{lstlisting}

Условный оператор с несколькими ветками:
\begin{lstlisting}
variable status: Text
value
   op: Int >< Int -~-> read status Int
   op(x,y) is
	if status = "sum" then
               x + y
        elsif status = "mul" then
               x * y
	else
		0
	end
\end{lstlisting}

\item оператор присваивания: используется для изменения значений глобальных переменных (аргументы функции переменными не являются, ими лишь поименованы значения)
\begin{lstlisting}
variable status : Text
value
  init : Unit -~-> write status Unit
  init() is (status := "initialized")	
\end{lstlisting}

Оператор присваивания имеет тип \textbf{Unit}.

\item последовательность операторов: через точку с запятой
\begin{lstlisting}
variable status : Text
value
  next : Int -~-> write status Int
  next() is
	status := "moved";
	x+1	
\end{lstlisting}
В этой функции сначала изменяется значение переменной \texttt{status}, а затем вычисляется выражение x+1. Значением последовательности операторов является значение последнего оператора. А все остальные элементы должны иметь тип \textbf{Unit}. Поэтому, например, следующая запись будет некорректной:
\begin{lstlisting}
variable status : Text
value
  next : Int -~-> write status Int
  next() is
        x+1;
	status := "moved"
\end{lstlisting}

\item операторы циклов: while, do-until и for
\begin{lstlisting}
variable a: Nat, b : Nat
value
  euclid: Unit -~-> write a, b Nat
  euclid() is
     while a > 0 /\ b > 0 do
        if a > b then a := a - b
        else b := b - a end
     end;
     if a = 0 then b else a end
\end{lstlisting}

\begin{lstlisting}
variable n: Nat, x : Nat
value
  digits: Unit -~-> write n, x Nat
  digits() is
     n := 0;
     do n := n + 1; x := x / 10
     while x = 0;
     n
\end{lstlisting}

\begin{lstlisting}
variable sum : Nat
value
  sumN: Nat -~-> write sum Unit
  sumN(n) is
	sum := 0;
        for i in <.1 .. n.> do
	  sum := sum + i
	end;
\end{lstlisting}

\begin{lstlisting}
variable sum : Nat
value
  sumN: Nat -~-> write sum Unit
  sumN(n) is
	sum := 0; i := 0;
    do
      i := i + 1;
      sum := sum + i
    until i = n	end;
\end{lstlisting}

Способов прервать цикл типа break в RSL нет.

\item локальные переменные:
\begin{lstlisting}
variable a: Nat, b : Nat
value
  euclid: Unit -~-> write a, b Nat
  euclid() is
   local variable a1: Nat := a,
                  b1: Nat := b in
     while a1 > 0 /\ b1 > 0 do
        if a1 > b1 then a1 := a1 - b1
        else b1 := b1 - a1 end
     end;
     if a1 = 0 then b1 else a1 end
   end
\end{lstlisting}

\item выражение \textbf{let}: не вводит локальные переменные! а вводит новые синонимы значений; кроме того, выполняет сопоставление с образцами (pattern matching):
явный \textbf{let}:
\begin{lstlisting}
value simple:  Int -~-> Int
  simple(x) is
    let y = abs x in y-x end
\end{lstlisting}

Выражение в \textbf{let} вычисляется один раз перед вычислением <<тела>> оператора \textbf{let}.

неявный \textbf{let}:
\begin{lstlisting}
value
  random: Nat -~-> Nat
  random(n) is
      let r : Nat :- r <= n in
	   r
      end	
\end{lstlisting}

\end{itemize}



\head{Массивы}
Следующая функция использует массив целых чисел:
\begin{lstlisting}
value sort: Int-list -~-> Int-list
\end{lstlisting}

Обращение по индексу делается так: A(1). Нумерация индексов \textbf{с единицы}. Операция \textbf{len} возвращает текущую длину массива. Массивы в RSL могут изменять длину (путем операции конкатенации). Индекс не должен иметь большее значение, чем длина массива, и меньшее, чем 1. Синтаксис RSL запрещает изменять значения отдельных элементов массивов (например, так: <<A(i) := i>>), можно только строить новые массивы целиком (например, вместо <<A(i) := e>> можно писать <<A := $\langle$ if k=i then e else A(k) end | k in $\langle$1 .. \textbf{len} A$\rangle$ $\rangle$>>).

\begin{lstlisting}
value
  sum: Int-list -~-> Int
  sum(ls) is
    local variable s : Int := 0 in
       for i in <.1 .. len ls.> do
             s := s + ls(i)
       end;
       s
    end;
\end{lstlisting}


Эту же функцию, суммирующую элементы массива, можно записать и без использования индексов:
\begin{lstlisting}
value
  sum: Int-list -~-> Int
  sum(ls) is
    local variable s : Int := 0 in
       for l in ls do
             s := s + l
       end;
       s
    end;
\end{lstlisting}

Тип \textbf{Text} является массивом из \textbf{Char}.

Операция \textbf{tl} возвращает <<подмассив>> --- от второго элемента до последнего элемента исходного массива. Операция определена только для непустых массивов. Пустой список обозначается символом <..>. Тем самым функцию sum можно записать следующим образом с использованием рекурсии:
\begin{lstlisting}
value
  sum: Int-list -~-> Int
  sum(ls) is
    if ls = <..> then 0
    else ls(1) + sum(tl ls) end
\end{lstlisting}


\head{Структуры}
\begin{lstlisting}
type FIO ::
         name : Text
         surname : Text
value
   hello: FIO -~-> Text
   hello(fio) is
      "Hello, " ^ name(fio) ^
           "  " ^ surname(fio) ^ "!"
\end{lstlisting}

Обращение к полю делается в виде вызова функции с именем поля.

\begin{lstlisting}
type FIO ::
         name : Text
         surname : Text
value
   new_fio: Text >< Text -~-> FIO
   new_fio(n,sn) is mk_FIO(n,sn)
\end{lstlisting}

Создание структуры делается с помощью функции с предопределенным именем. Это имя начинается с <<mk\_>>, за которым идет имя типа структуры. В скобках подряд перечисляются выражения, дающие значения полям новой структуры.

\head{Перечисления (enumeration)}
\begin{lstlisting}
type Color = red | blue | white | green
value
  from_rus : Color -~-> Bool
  from_rus(c) is c = red \/ c = blue \/ c = white
\end{lstlisting}

\head{Указатели}
RSL не содержит встроенных механизмов для задания алгоритмов, работающих с указателями.
